Hyperproperties express the relationship between multiple executions of a
system. This is needed in many AI-related fields, such as knowledge
representation and planning, to capture system properties related to knowledge,
information flow, and privacy. In this paper, we study the monitoring of
complex hyperproperties at runtime. Previous work in this area has either
focused on the simpler problem of monitoring trace properties (which are sets
of traces, while hyperproperties are sets of sets of traces) or on monitoring
first-order hyperproperties, which are expressible in temporal logics with
first-order quantification over traces, such as HyperLTL. We present the first
monitoring algorithm for the much more expressive class of second-order
hyperproperties. Second-order hyperproperties include system properties like
common knowledge, which cannot be expressed in first-order logics like
HyperLTL.
We introduce Hyper$^2$LTL$_f$, a temporal logic over finite traces that
allows for second-order quantification over sets of traces. We study the
monitoring problem in two fundamental execution models: (1) the parallel model,
where a fixed number of traces is monitored in parallel, and (2) the sequential
model, where an unbounded number of traces is observed sequentially, one trace
after the other. For the parallel model, we show that the monitoring of the
second-order hyperproperties of Hyper$^2$LTL$_f$ can be reduced to monitoring
first-order hyperproperties. For the sequential model, we present a monitoring
algorithm that handles second-order quantification efficiently, exploiting
optimizations based on the monotonicity of subformulas, graph-based storing of
executions, and fixpoint hashing. We present experimental results from a range
of benchmarks, including examples from common knowledge and planning.

本文研究了复杂超性质的运行时监测问题，并提出了第一个适用于更具表达能力的二阶超性质的监测算法 Hyper$^2$LTL$_f$。我们探讨了并行模型和顺序模型下的监测问题，并通过优化算法提高了二阶量化的效率。实验结果验证了算法的有效性。